CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates

摘要

Termination is an important property of programs; notably required forprograms formulated in proof assistants. It is a very active subject ofresearch in the Turing-complete formalism of term rewriting systems, where manymethods and tools have been developed over the years to address this problem.Ensuring reliability of those tools is therefore an important issue. In thispaper we present a library formalizing important results of the theory ofwell-founded (rewrite) relations in the proof assistant Coq. We also presentits application to the automated verification of termination certificates, asproduced by termination tools.